IrrelevantTelescope.agda:6,10-11
Variable A is declared irrelevant, so it cannot be used here
when checking that the expression A has type _1 _
